Inference at * 1 
Iof proof for Lemma nil fseg:



1. T : Type
2. l : T List
  l = (l @ []) 

latex

 by ((RWO "append_nil_sq" 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	as @ bs, s ~ t, S  T, x:A. B(x), x:AB(x), s = t, type List, Type, Top, x:A.B(x), t  T, Void
Lemmas	append nil sq, member wf, top wf